g, h:IMonoid, f:MonHom(g,h), n:, u:|g|. (n  (f(u))) = f(n  u)  |h| 

latex

Up	groups 1
Definitions of Statement	IMonoid, IsMonHom{M1,M2}(f), MonHom(M1,M2)
Definitions	t  T, x:A. B(x), False, A, A  B, P  Q, P & Q, P  Q, P  Q, , , x f y, IMonoid, FunThru2op(A;B;opa;opb;f), IsMonHom{M1,M2}(f), MonHom(M1,M2),
Lemmas	imon wf, monoid hom wf, nat wf, grp car wf, le wf, monoid hom properties, mon nat op zero, mon nat op unroll, mon nat op wf, grp op wf